STAMP - 2019 - Annual activity report

STAMP

STAMP - 2019

Project-Team Stamp

Team, Visitors, External Collaborators

Overall Objectives

Research Program

Theoretical background

Application Domains

Mathematical Components
Proofs in cryptography
Proofs for robotics

New Software and Platforms

Coq
Math-Components
Semantics
Easycrypt
ELPI
Coq-elpi
AutoGnP
MaskComp
Jasmin
MaskVerif
CoqEAL
math-comp-analysis
math-comp-finmap
math-comp-real-closed

New Results

Hol-Light and Elpi
Generating equality tests for inductive types
Re-designing the state machine of Coq
Formal proofs on session types
Formal proofs of an axiomatization of graphs with tree-width two
Formal study of double-word arithmetic algorithms
Approximations using Chebyshev polynomials
Formalizing computational analysis
Formal study of probabilistic programs
Security of a key management service
High-assurance and high-speed SHA-3
A domain-specific language for timing sensitive computation
Proving equivalence between probabilistic programs
MaskVerif: automated verification of higher-order masking in presence of physical defaults
Frame type theory
Automated refinements on algorithms in Lean
Parametricity in Template Coq
A hierarchy builder
Adding measure theory to mathematical components analysis
A formal description of exact real arithmetic
Formal study of a triangulation algorithm
Formal study of Voronoi diagrams and Fortune's algorithm
Formal study of a cell-decomposition algorithm
A guide to use Coq for security evaluations
Formalization of the Poincaré disk model in Isabelle
Integration of the GeoCoq library to Logipedia
Performance improvements for a reflective tactic in the GeoCoq library
Mutual interpretability of cartesian planes with Tarski's system of geometry
Simplification of a constructive version of Tarski's system of geometry
Formal proofs of Tarjan's strongly connected components algorithm

Partnerships and Cooperations

National Initiatives
European Initiatives
International Initiatives
International Research Visitors

Dissemination

Promoting Scientific Activities
Teaching - Supervision - Juries
Popularization

Bibliography

Publications of the year
References in notes

Previous |

Home | Next next

Section: New Results

Hol-Light and Elpi

Participants : Enrico Tassi, Marco Maggesi [University of Florence, Italy] .

We implemented an elaborator for HOL-Light in Elpi. In particular the new elaborator supports coercions and overloaded notations for algebraic structures.

Previous |

Home | Next next